Conversation
|
On further investigation, this is unlikely to be breaking. It makes I haven't looked into whether other code uses EDIT: I guess technically there might be code with |
There was a problem hiding this comment.
Pull request overview
Fixes a bug where EqTest.for_expr exposed only the syntactic (alpha-equivalence based) expression equality from EqTest_base, while the convertibility-based for_expr provided to EqMod_base was only being used internally by for_instr / for_stmt. Replacing open Fe with include Fe re-exports the convertibility-aware for_expr so the outer EqTest.for_expr (line 1895) binds to the intended version.
Changes:
- Switch
open Fetoinclude FeinEqMod_baseso itsfor_expris part of the module's signature and overrides the syntactic version inherited fromEqTest_base. - Hoist creation of the
&dummymemory identifier out of the innerconvertclosure so it is shared betweene1ande2(previously a fresh ident was created for each side).
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
This was already being done when checking equality of instructions and statements, but not expressions.
It seems like this was an accident. The
EqTestmodule exposes thefor_exprdefinition used by the internalEqTest_basewhile defining its own that ends up being used byfor_instrandfor_stmt. The relevant line number is 1896.It's likely that this will break something, but I don't have an example. I found this while trying to fix #990, but AFAICT this change won't break any uses of
simby itself. See also #997.